Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix #10042 Don't recommend deprecated/removed 'extensions:' field #10044

Merged
merged 1 commit into from
May 28, 2024

Conversation

mpilgrem
Copy link
Collaborator

Related issue:

Include the following checklist in your PR:

  • Patches conform to the coding conventions.
  • Any changes that could be relevant to users have been recorded in the changelog.
  • The documentation has been updated, if necessary. Not necessary.
  • Manual QA notes have been included. None needed.
  • Tests have been added. (Ask for help if you don’t know how to write them! Ask for an exemption if tests are too complex for too little coverage!) None needed.

@mpilgrem
Copy link
Collaborator Author

I think the CI is failing for reasons unconnected with this pull request.

@mpilgrem mpilgrem requested a review from ulysses4ever May 23, 2024 07:01
@geekosaur
Copy link
Collaborator

Yes, we're working on it.

Copy link
Collaborator

@ulysses4ever ulysses4ever left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Awesome!

@ulysses4ever
Copy link
Collaborator

ulysses4ever commented May 23, 2024

@geekosaur I don't know that anyone is working on the changelog.d/GHC 9.10 failure btw! Maybe you could give it a try? Hécate suggested that instead of building it, we could just download a bindists...

@ulysses4ever
Copy link
Collaborator

I stand corrected: the changelog-d issue is being worked on here: #10048

@mpilgrem
Copy link
Collaborator Author

I've rebased on master.

@ulysses4ever
Copy link
Collaborator

@mpilgrem awesome! Per CONTRIBUTING.md, do you want to apply a merge label (either merge me or squash+merge). Squashing makes more sense, I think.

@mpilgrem mpilgrem added merge me Tell Mergify Bot to merge and removed merge me Tell Mergify Bot to merge labels May 26, 2024
@mpilgrem mpilgrem added the merge me Tell Mergify Bot to merge label May 26, 2024
@mpilgrem
Copy link
Collaborator Author

I've tidied-up manually.

@mergify mergify bot added the merge delay passed Applied (usually by Mergify) when PR approved and received no updates for 2 days label May 28, 2024
@mergify mergify bot merged commit 88c81c9 into master May 28, 2024
51 checks passed
@mergify mergify bot deleted the fix10042 branch May 28, 2024 07:58
@ulysses4ever
Copy link
Collaborator

@mergify backport 3.12

Copy link
Contributor

mergify bot commented Jun 6, 2024

backport 3.12

✅ Backports have been created

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
merge delay passed Applied (usually by Mergify) when PR approved and received no updates for 2 days merge me Tell Mergify Bot to merge
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Cabal (the library) advises use of extensions: when that field is deprecated
3 participants